The present invention relates generally to hardware verification for electronic circuit designs. More particularly, the present invention relates to using local reduction in model checking to identify faults in logically correct circuits.
Recent advances in the design of application specific integrated circuits (ASIC) and system-on-chip (SoC) circuits are producing circuit designs of rapidly increasing complexity. These designs are driving the search for techniques that are capable of verifying such complex designs.
One commonly-used verification technique is model checking, which employs exhaustive mathematical techniques to prove whether a property holds true for a given design. A model checker uses a model of the design to consider all possible input combinations, and covers all possible reachable states to verify a property of the design. This is possible due to efficient techniques such as symbolic model checking and Binary Decision Diagram (BDD) representation used in model checking tools that allow analysis of sets of states simultaneously, and only consider the logic in the cone of influence of the property the tool is verifying.
However, conventional model checking tools verify only the logical design of a circuit. A circuit that is logically correct can still fail due to problems with timing, crosstalk, and other electrical anomalies. Conventional model checking tools are unable to detect such failures.